Comparing State Spaces in Automatic Security Protocol Analysis
Identifieur interne : 003982 ( Main/Exploration ); précédent : 003981; suivant : 003983Comparing State Spaces in Automatic Security Protocol Analysis
Auteurs : Cas J. F. Cremers [Suisse] ; Pascal Lafourcade [France] ; Philippe Nadeau [Autriche]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: There are several automatic tools available for the symbolic analysis of security protocols. The models underlying these tools differ in many aspects. Some of the differences have already been formally related to each other in the literature, such as difference in protocol execution models or definitions of security properties. However, there is an important difference between analysis tools that has not been investigated in depth before: the explored state space. Some tools explore all possible behaviors, whereas others explore strict subsets, often by using so-called scenarios. We identify several types of state space explored by protocol analysis tools, and relate them to each other. We find previously unreported differences between the various approaches. Using combinatorial results, we determine the requirements for emulating one type of state space by combinations of another type. We apply our study of state space relations in a performance comparison of several well-known automatic tools for security protocol analysis. We model a set of protocols and their properties as homogeneously as possible for each tool. We analyze the performance of the tools over comparable state spaces. This work enables us to effectively compare these automatic tools, i.e., using the same protocol description and exploring the same state space. We also propose some explanations for our experimental results, leading to a better understanding of the tools.
Url:
DOI: 10.1007/978-3-642-02002-5_5
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003501
- to stream Istex, to step Curation: 003459
- to stream Istex, to step Checkpoint: 000A89
- to stream Main, to step Merge: 003A60
- to stream Main, to step Curation: 003982
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Comparing State Spaces in Automatic Security Protocol Analysis</title><author><name sortKey="Cremers, Cas J F" sort="Cremers, Cas J F" uniqKey="Cremers C" first="Cas J. F." last="Cremers">Cas J. F. Cremers</name></author><author><name sortKey="Lafourcade, Pascal" sort="Lafourcade, Pascal" uniqKey="Lafourcade P" first="Pascal" last="Lafourcade">Pascal Lafourcade</name></author><author><name sortKey="Nadeau, Philippe" sort="Nadeau, Philippe" uniqKey="Nadeau P" first="Philippe" last="Nadeau">Philippe Nadeau</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:DE59AC3AF43E66D9798E2904A3809061E6FD0FD8</idno><date when="2009" year="2009">2009</date><idno type="doi">10.1007/978-3-642-02002-5_5</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-B1GX2F58-B/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003501</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003501</idno><idno type="wicri:Area/Istex/Curation">003459</idno><idno type="wicri:Area/Istex/Checkpoint">000A89</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000A89</idno><idno type="wicri:doubleKey">0302-9743:2009:Cremers C:comparing:state:spaces</idno><idno type="wicri:Area/Main/Merge">003A60</idno><idno type="wicri:Area/Main/Curation">003982</idno><idno type="wicri:Area/Main/Exploration">003982</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Comparing State Spaces in Automatic Security Protocol Analysis</title><author><name sortKey="Cremers, Cas J F" sort="Cremers, Cas J F" uniqKey="Cremers C" first="Cas J. F." last="Cremers">Cas J. F. Cremers</name><affiliation wicri:level="1"><country xml:lang="fr">Suisse</country><wicri:regionArea>Department of Computer Science, ETH Zurich, 8092, Zurich</wicri:regionArea><wicri:noRegion>Zurich</wicri:noRegion></affiliation></author><author><name sortKey="Lafourcade, Pascal" sort="Lafourcade, Pascal" uniqKey="Lafourcade P" first="Pascal" last="Lafourcade">Pascal Lafourcade</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Verimag, University of Grenoble, 38610, Giéres</wicri:regionArea><placeName><region type="region" nuts="2">Auvergne-Rhône-Alpes</region><region type="old region" nuts="2">Rhône-Alpes</region><settlement type="city">Giéres</settlement></placeName></affiliation></author><author><name sortKey="Nadeau, Philippe" sort="Nadeau, Philippe" uniqKey="Nadeau P" first="Philippe" last="Nadeau">Philippe Nadeau</name><affiliation wicri:level="1"><country xml:lang="fr">Autriche</country><wicri:regionArea>Faculty of Mathematics of the University of Vienna</wicri:regionArea></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: There are several automatic tools available for the symbolic analysis of security protocols. The models underlying these tools differ in many aspects. Some of the differences have already been formally related to each other in the literature, such as difference in protocol execution models or definitions of security properties. However, there is an important difference between analysis tools that has not been investigated in depth before: the explored state space. Some tools explore all possible behaviors, whereas others explore strict subsets, often by using so-called scenarios. We identify several types of state space explored by protocol analysis tools, and relate them to each other. We find previously unreported differences between the various approaches. Using combinatorial results, we determine the requirements for emulating one type of state space by combinations of another type. We apply our study of state space relations in a performance comparison of several well-known automatic tools for security protocol analysis. We model a set of protocols and their properties as homogeneously as possible for each tool. We analyze the performance of the tools over comparable state spaces. This work enables us to effectively compare these automatic tools, i.e., using the same protocol description and exploring the same state space. We also propose some explanations for our experimental results, leading to a better understanding of the tools.</div></front></TEI><affiliations><list><country><li>Autriche</li><li>France</li><li>Suisse</li></country><region><li>Auvergne-Rhône-Alpes</li><li>Rhône-Alpes</li></region><settlement><li>Giéres</li></settlement></list><tree><country name="Suisse"><noRegion><name sortKey="Cremers, Cas J F" sort="Cremers, Cas J F" uniqKey="Cremers C" first="Cas J. F." last="Cremers">Cas J. F. Cremers</name></noRegion></country><country name="France"><region name="Auvergne-Rhône-Alpes"><name sortKey="Lafourcade, Pascal" sort="Lafourcade, Pascal" uniqKey="Lafourcade P" first="Pascal" last="Lafourcade">Pascal Lafourcade</name></region></country><country name="Autriche"><noRegion><name sortKey="Nadeau, Philippe" sort="Nadeau, Philippe" uniqKey="Nadeau P" first="Philippe" last="Nadeau">Philippe Nadeau</name></noRegion></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003982 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 003982 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:DE59AC3AF43E66D9798E2904A3809061E6FD0FD8
|texte= Comparing State Spaces in Automatic Security Protocol Analysis
}}
| This area was generated with Dilib version V0.6.33. |  |